$\forall$$E$,$X_{1}$,$X_{2}$:Type, ${\it info}$:($E$$\rightarrow$((:Id $\times$ $X_{1}$) + (:(:IdLnk $\times$ $E$) $\times$ $X_{2}$))), ${\it pred?}$:($E$$\rightarrow$(?$E$)), $e$,${\it e'}$:$E$.
\\[0ex]pred!($e$;${\it e'}$) $\in$ prop\{i:l\}